T:Type, L:T List, P:(||L||Prop).
(x:||L||. Dec(P(x)))
 (i, j:||L||. P(i)  i<j  P(j))
 (L_1, L_2:T List. L = (L_1 @ L_2) & (i:||L||. P(i)  ||L_1||i)) 

latex

Definitions	{i..j}, P  Q, x:A. B(x), P & Q, x:A. B(x), P  Q, False, A, AB, t  T, i  j < k, ||as||, Prop, P  Q, Dec(P), x. t(x), as @ bs, firstn(n;as), P  Q, nth_tl(n;as), {i...j}, True, T, {T}, SQType(T)
Lemmas	int seg properties, append back nil, decidable int equal, squash wf, true wf, length firstn, decidable le, append firstn lastn, firstn wf, nth tl wf, append wf, iff wf, decidable wf, length wf1, decidable ex int seg, decidable cand, decidable all int seg, decidable not, not wf, le wf, int seg wf